1. Technical Field
This disclosure relates to electronic design automation (EDA). Specifically, this disclosure relates to methods and systems for performing an abstraction-based livelock/deadlock checking for a circuit design during a formal verification of the design.
2. Related Art
Livelock/deadlock checking is a difficult problem in hardware verification. A “livelock” refers to a set of states from which there is no path going to any other state that is reachable from the initial states of a design. In other words, when a design reaches a livelock, the design becomes permanently stuck at one or a few states. Note that a “deadlock” is a special case of the livelock when the number of states in the livelock is one. On the other hand, a “toggle deadlock” is a state for a sequential element in the livelock, wherein the sequential element initially toggles, but eventually sticks to a constant value (either 0 or 1).
Livelocks and toggle deadlocks are important design properties to verify in a hardware design. To check whether a livelock or a toggle deadlock exists in a design, ideally the checking should be performed on the whole design. However, the large size and high complexity of real designs have made it impractical to check the whole design. While some conventional techniques can handle up to a few hundred sequential elements, real designs often contain hundreds of thousands of sequential elements.
Hence, what is needed are a method and a system for performing livelock/deadlock checking on real designs without the above-described problems.